locl(a) sends [tg,f{AT}(x)] on link l once
== vartype(source(l);x)  A & (e:E. kind(e) = rcv(l,tg)  valtype(e)  T)
== & (e:E.
== & (kind(e) = rcv(l,tg)
== & (& val(e) = f(x when sender(e))
== & (& & kind(sender(e)) = locl(a)
== & (& & (e':E. kind(e') = rcv(l,tg)  kind(sender(e')) = locl(a)  e' = e)) 

latex

---

clarification:

send-once-p(es;T;A;a;l;tg;f;x)
== es-vartype(es; source(l); x)  A
== & (e:es-E(es). es-kind(es; e) = rcv(l,tg)  Knd  es-valtype(es; e)  T)
== & (e:es-E(es).
== & (es-kind(es; e) = rcv(l,tg)  Knd
== & (& es-val(es; e) = f(es-when(es; x; es-sender(es; e)))  T
== & (& & es-kind(es; es-sender(es; e)) = locl(a)  Knd
== & (& & (e':es-E(es).
== & (& & (es-kind(es; e') = rcv(l,tg)  Knd
== & (& & ( es-kind(es; es-sender(es; e')) = locl(a)  Knd
== & (& & ( e' = e  es-E(es))) 

latex

Definitions	vartype(i;x), source(l), valtype(e), x:A. B(x), A & B, val(e), f(a), x when e, P & Q, x:A. B(x), rcv(l,tg), P  Q, Knd, kind(e), sender(e), locl(a), s = t, E
FDL editor aliases	send-once-p